\begin{tabbing}
$\forall$${\it es}$:ES, $R$:(E$\rightarrow$E$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$e$, ${\it e'}$:E. Dec($R$(${\it e'}$,$e$)))
\\[0ex]$\Rightarrow$ $R$ =$>$ $\lambda$$x$,$y$. ($x$ $<$ $y$)
\\[0ex]$\Rightarrow$ \=($\forall$$e$, ${\it e'}$:E.\+
\\[0ex](${\it e'}$ $R$ $e$) $\Rightarrow$ ($\neg$es{-}r{-}immediate{-}pred(${\it es}$;$R$;${\it e'}$;$e$)) $\Rightarrow$ ($\exists$$c$:E. ((${\it e'}$ $R$ $c$) \& ($c$ $R$ $e$))))
\-
\end{tabbing}